ecl-halt(ds;da;x)
== ecl_ind(x;k,test.n,L. n = 0
== & (L':event-info(ds;da) List, s:State(ds), v:Valtype(da;k).
== & (L = (L' @ [<k,s,v>]) & test(s,v)
== & (& (tL'. let k',s,v = t in k = k' & test(s,v)));a,b,ha,hb.n,L. 0<n & ha(n,L)
==  (L1, L2:event-info(ds;da) List. L = (L1 @ L2) & ha(0,L1) & hb(n,L2));a,b,ha,hb.n,L.
== (n = 0
== ( ha(0,L) & (L':event-info(ds;da) List. L'  L & hb(0,L'))
== (  hb(0,L) & (L':event-info(ds;da) List. L'  L & ha(0,L')))
== & (0<n
== & ( ha(n,L) & (m:, L':event-info(ds;da) List. L'  L  hb(m,L')  L' = L & nm)
== & (  hb(n,L)
== & (  & (m:, L':event-info(ds;da) List. L'  L  ha(m,L')  L' = L & nm));a,b,ha,hb.n,L.
== ha(n,L) & (m:, L':event-info(ds;da) List. L'  L  hb(m,L')  L' = L & nm)
==  hb(n,L) & (m:, L':event-info(ds;da) List. L'  L  ha(m,L')  L' = L & nm);a,ha.n,L. 0<n
== & star-append(event-info(ds;da);ha(0);ha(n))(L);a,m,ha.ha;a,m,ha.n,L. 0<n & ha(n,L)
==  n = m & ha(0,L);a,l,ha.n,L. ha(n,L) & (n  l)  n = 0 & (ml.ha(m,L))) 

latex

---

clarification:

ecl-halt(ds;da;x)
== ecl_ind(x;k,test.n,L. n = 0  
== & (L':event-info(ds;da) List, s:State(ds), v:Valtype(da;k).
== & (L = (L' @ (<k,s,v>.nil))  event-info(ds;da) List & test(s,v)
== & (& l_all(L';event-info(ds;da);t.let k',s,v = t in k = k'  Knd & test(s,v)));a,b,ha,hb.n,L.
== 0<n & ha(n,L)
==  (L1:event-info(ds;da) List, L2:event-info(ds;da) List.
==  (L = (L1 @ L2)  event-info(ds;da) List & ha(0,L1) & hb(n,L2));a,b,ha,hb.n,L.
== (n = 0  
== ( ha(0,L) & (L':event-info(ds;da) List. L'  L  event-info(ds;da) List & hb(0,L'))
== (  hb(0,L) & (L':event-info(ds;da) List. L'  L  event-info(ds;da) List & ha(0,L')))
== & (0<n
== & ( ha(n,L)
== & ( & (m:, L':event-info(ds;da) List.
== & ( & (L'  L  event-info(ds;da) List  hb(m,L')  L' = L  event-info(ds;da) List & nm)
== & (  hb(n,L)
== & (  & (m:, L':event-info(ds;da) List.
== & (  & (L'  L  event-info(ds;da) List
== & (  & ( ha(m,L')
== & (  & ( L' = L  event-info(ds;da) List & nm));a,b,ha,hb.n,L. ha(n,L)
== & (m:, L':event-info(ds;da) List.
== & (L'  L  event-info(ds;da) List  hb(m,L')  L' = L  event-info(ds;da) List & nm)
==  hb(n,L)
==  & (m:, L':event-info(ds;da) List.
==  & (L'  L  event-info(ds;da) List
==  & ( ha(m,L')
==  & ( L' = L  event-info(ds;da) List & nm);a,ha.n,L. 0<n
== & star-append(event-info(ds;da);ha(0);ha(n))(L);a,m,ha.ha;a,m,ha.n,L. 0<n & ha(n,L)
==  n = m   & ha(0,L);a,l,ha.n,L. ha(n,L) & (n  l  )
==  n = 0   & l_exists(l;;m.ha(m,L))) 

latex

Definitions	ecl ind, State(ds), Valtype(da;k), car.cdr, <a,b>, nil, xL. P(x), let x,y,z = a in t(x;y;z), A & B, Knd, b, as @ bs, x:A. B(x), x:A. B(x), l1  l2, P  Q, type List, AB, star-append(T;P;Q), event-info(ds;da), a<b, x.A(x), P  Q, A, (x  l), P & Q, s = t, , #$n, (xL.P(x)), , f(a)
FDL editor aliases	ecl-halt